﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using Epsilon.Expr;

namespace Epsilon.Typing
{
    public partial class TypeChecker
    {
        public TypeLabel TypeCheck(Context c, Expression e)
        {
            if (e is AtomExpr)
                return TypeCheck(c, (AtomExpr)e);
            else if (e is PidExpr)
                return TypeCheck(c, (PidExpr)e);
            else if (e is IntExpr)
                return TypeCheck(c, (IntExpr)e);
            else if (e is BoolExpr)
                return TypeCheck(c, (BoolExpr)e);
            else if (e is StringExpr)
                return TypeCheck(c, (StringExpr)e);
            else if (e is UnitExpr)
                return TypeCheck(c, (UnitExpr)e);
            else if (e is PreOpExpr)
                return TypeCheck(c, (PreOpExpr)e);
            else if (e is TupleExpr)
                return TypeCheck(c, (TupleExpr)e);
            else if (e is ProjExpr)
                return TypeCheck(c, (ProjExpr)e);
            else if (e is BinOpExpr)
                return TypeCheck(c, (BinOpExpr)e);
            else if (e is NilExpr)
                return TypeCheck(c, (NilExpr)e);
            else if (e is ListExpr)
                return TypeCheck(c, (ListExpr)e);
            else if (e is ListTailExpr)
                return TypeCheck(c, (ListTailExpr)e);
            else if (e is ListOpExpr)
                return TypeCheck(c, (ListOpExpr)e);
            else if (e is SeqExpr)
                return TypeCheck(c, (SeqExpr)e);
            else if (e is ParenExpr)
                return TypeCheck(c, (ParenExpr)e);
            else if (e is VarExpr)
                return TypeCheck(c, (VarExpr)e);
            else if (e is SelfExpr)
                return TypeCheck(c, (SelfExpr)e);
            else if (e is ScOpExpr)
                return TypeCheck(c, (ScOpExpr)e);
            else if (e is IfExpr)
                return TypeCheck(c, (IfExpr)e);
            else if (e is ListCaseExpr)
                return TypeCheck(c, (ListCaseExpr)e);
            else if (e is RecordExpr)
                return TypeCheck(c, (RecordExpr)e);
            else if (e is RecModExpr)
                return TypeCheck(c, (RecModExpr)e);
            else if (e is RecProjExpr)
                return TypeCheck(c, (RecProjExpr)e);
            else if (e is FunExpr)
                return TypeCheck(c, (FunExpr)e);
            else if (e is FunctionExpr)
                return TypeCheck(c, (FunctionExpr)e);
            else if (e is ApplyExpr)
                return TypeCheck(c, (ApplyExpr)e);
            else if (e is LabExpr)
                return TypeCheck(c, (LabExpr)e);
            else if (e is SpawnExpr)
                return TypeCheck(c, (SpawnExpr)e);
            else if (e is RxExpr)
                return TypeCheck(c, (RxExpr)e);
            else if (e is TxExpr)
                return TypeCheck(c, (TxExpr)e);
            else
                Error("Invalid expression", e);
            return null;
        }

        public TypeLabel TypeCheck(Context c, AtomExpr e)
        {
            TypeLabel tl = new TypeLabel(
                new AtomType(e.Value),
                new PidBase(null, null),
                new PidBase(null, null),
                new SecBase(null, null)
                );

            e.Label = tl;
            return tl;
        }

        public TypeLabel TypeCheck(Context c, PidExpr e)
        {
            List<PidExpr> pe = new List<PidExpr>();
            pe.Add(e);

            TypeLabel tl = new TypeLabel(
                new SimpleType(BaseType.Pid),
                new PidBase(null, pe),        
                new PidBase(null, pe),        
                new SecBase(null, null)       
                );

            e.Label = tl;
            return tl;
        }

        public TypeLabel TypeCheck(Context c, IntExpr e)
        {
            TypeLabel tl = new TypeLabel(
                new SimpleType(BaseType.Int), 
                new PidBase(null, null),      
                new PidBase(null, null),      
                new SecBase(null, null)       
                );

            e.Label = tl;
            return tl;
        }

        public TypeLabel TypeCheck(Context c, BoolExpr e)
        {
            TypeLabel tl = new TypeLabel(
                new SimpleType(BaseType.Bool),
                new PidBase(null, null),
                new PidBase(null, null),
                new SecBase(null, null)
                );

            e.Label = tl;
            return tl;
        }

        public TypeLabel TypeCheck(Context c, StringExpr e)
        {
            TypeLabel tl = new TypeLabel(
                new SimpleType(BaseType.String),
                new PidBase(null, null),
                new PidBase(null, null),
                new SecBase(null, null)
                );

            e.Label = tl;
            return tl;
        }

        public TypeLabel TypeCheck(Context c, UnitExpr e)
        {
            TypeLabel tl = new TypeLabel(
                new SimpleType(BaseType.Unit),
                new PidBase(null, null),
                new PidBase(null, null),
                new SecBase(null, null)
                );

            e.Label = tl;
            return tl;
        }

        public TypeLabel TypeCheck(Context c, PreOpExpr e)
        {
            TypeLabel t = TypeCheck(c, e.Operand);

            Type tp = null;

            if (e.Op == PreOp.Plus || e.Op == PreOp.Minus || e.Op == PreOp.BNOT)
            {
                if (t.Type == SimpleType.IntType)
                    tp = new SimpleType(BaseType.Int);
                else
                    Error("Expected an integer, found " + t.Type.ToString(), e);
            }
            else if (e.Op == PreOp.NOT)
            {
                if (t.Type == SimpleType.BoolType)
                    tp = new SimpleType(BaseType.Bool);
                else
                    Error("Expected a boolean, found " + t.Type.ToString(), e);
            }
            else
            {
                Error("Invalid operation found", e);
            }

            TypeLabel tl = new TypeLabel(
                tp,
                new PidBase(null, null),
                new PidBase(null, null),
                t.SecLabel
                );

            e.Label = tl;
            return tl;
        }

        public TypeLabel TypeCheck(Context c, BinOpExpr e)
        {
            TypeLabel t1 = TypeCheck(c, e.Left);
            TypeLabel t2 = TypeCheck(c, e.Right);

            Type tp = null;

            if (e.Op == BinOp.Plus || e.Op == BinOp.Minus ||
                e.Op == BinOp.BAND || e.Op == BinOp.BOR || e.Op == BinOp.BXOR ||
                e.Op == BinOp.BSL || e.Op == BinOp.BSR)
            {
                if (t1.Type == SimpleType.IntType && t2.Type == SimpleType.IntType)
                    tp = new SimpleType(BaseType.Int);
                else
                    Error("Expected two integers, found " + t1.Type.ToString() +
                        " and " + t2.Type.ToString(), e);
            }
            else if (e.Op == BinOp.Equals || e.Op == BinOp.NotEquals ||
                e.Op == BinOp.GreaterThan || e.Op == BinOp.GreaterThanOrEqual ||
                e.Op == BinOp.LessThan || e.Op == BinOp.LessThanOrEqual)
            {
                if (t1.Type == SimpleType.IntType && t2.Type == SimpleType.IntType)
                    tp = new SimpleType(BaseType.Bool);
                else
                    Error("Expected two integers, found " + t1.Type.ToString() +
                        " and " + t2.Type.ToString(), e);
            }
            else if (e.Op == BinOp.AND || e.Op == BinOp.OR || e.Op == BinOp.XOR)
            {
                if (t1.Type == SimpleType.BoolType && t2.Type == SimpleType.BoolType)
                    tp = new SimpleType(BaseType.Bool);
                else
                    Error("Expected two booleans, found " + t1.Type.ToString() +
                        " and " + t2.Type.ToString(), e);
            }
            else
            {
                Error("Invalid operation found", e);
            }

            TypeLabel tl = new TypeLabel(
                tp,
                new PidBase(null, null),
                new PidBase(null, null),
                SecUtil.Meet(t1.SecLabel, t2.SecLabel)
                );

            e.Label = tl;
            return tl;
        }

        public TypeLabel TypeCheck(Context c, TupleExpr e)
        {
            List<Type> t = new List<Type>();
            List<PidLabel> p1 = new List<PidLabel>();
            List<PidLabel> p2 = new List<PidLabel>();
            List<SecLabel> k = new List<SecLabel>();

            for (int i = 0; i < e.Expressions.Count; i++)
            {
                TypeLabel l = TypeCheck(c, e.Expressions[i]);
                t.Add(l.Type);
                p1.Add(l.MaxPidLabel);
                p2.Add(l.MinPidLabel);
                k.Add(l.SecLabel);
            }

            TypeLabel tl = new TypeLabel(
                new TupleType(t),
                new PidTuple(p1),
                new PidTuple(p2),
                new SecTuple(k)
                );

            e.Label = tl;
            return tl;
        }

        public TypeLabel TypeCheck(Context c, ProjExpr e)
        {
            TypeLabel l = TypeCheck(c, e.Tuple);
            if (!((l.Type is TupleType) || (l.MaxPidLabel is PidLabel) ||
                (l.MinPidLabel is PidLabel) || (l.SecLabel is SecLabel)))
                Error("Expression does not return a tuple", e);

            if (e.Element < 1 || e.Element > ((TupleType)(l.Type)).Types.Count)
                Error("Invalid element index", e);

            TypeLabel tl = new TypeLabel(
                ((TupleType)(l.Type)).Types[e.Element - 1],
                ((PidTuple)(l.MaxPidLabel)).Labels[e.Element - 1],
                ((PidTuple)(l.MinPidLabel)).Labels[e.Element - 1],
                ((SecTuple)(l.SecLabel)).Labels[e.Element - 1]
                );

            e.Label = tl;
            return tl;
        }

        public TypeLabel TypeCheck(Context c, NilExpr e)
        {
            TypeLabel tl = new TypeLabel(
                new ListType(e.Type),
                new PidBase(null, null),
                new PidBase(null, null),
                new SecBase(null, null)
                );

            e.Label = tl;
            return tl;
        }

        public TypeLabel TypeCheck(Context c, ListExpr e)
        {
            if (e.Elements.Count == 0)
                Error("A list must contain at least one element", e);

            List<TypeLabel> labels = new List<TypeLabel>();
            for (int i = 0; i < e.Elements.Count; i++)
                labels.Add(TypeCheck(c, e.Elements[i]));

            Type elementType = labels[0].Type;
            for (int i = 1; i < labels.Count; i++)
            {
                if (labels[i].Type != elementType)
                    Error("Lists must contain elements of a single type", e);
            }

            TypeLabel tl = JoinMeet(new ListType(elementType), labels);

            e.Label = tl;
            return tl;
        }

        public TypeLabel TypeCheck(Context c, ListTailExpr e)
        {
            if (e.Elements.Count == 0)
                Error("A list must contain at least one element before the tail", e);

            List<TypeLabel> labels = new List<TypeLabel>();
            for (int i = 0; i < e.Elements.Count; i++)
                labels.Add(TypeCheck(c, e.Elements[i]));

            Type elementType = labels[0].Type;
            for (int i = 1; i < labels.Count; i++)
            {
                if (labels[i].Type != elementType)
                    Error("Lists must contain elements of a single type", e);
            }

            TypeLabel tail = TypeCheck(c, e.Tail);
            if ((new ListType(elementType)) != tail.Type)
                Error("Tail type does not match element type", e);

            labels.Add(tail);

            TypeLabel tl = JoinMeet(tail.Type, labels);

            e.Label = tl;
            return tl;
        }

        public TypeLabel TypeCheck(Context c, ListOpExpr e)
        {
            TypeLabel t1 = TypeCheck(c, e.Left);
            TypeLabel t2 = TypeCheck(c, e.Right);

            ListType t = new ListType(e.Type);
            if (t1.Type != t || t2.Type != t)
                Error("Operands do not have the correct type", e);

            PidLabel pmax = null;
            PidLabel pmin = null;
            SecLabel sec = SecUtil.Meet(t1.SecLabel, t2.SecLabel);

            if (e.Op == ListOp.Concat)
            {
                pmax = PidUtil.Join(t1.MaxPidLabel, t2.MaxPidLabel);
                pmin = PidUtil.Meet(t1.MinPidLabel, t2.MinPidLabel);
            }
            else if (e.Op == ListOp.Diff)
            {
                pmax = t1.MaxPidLabel;
                pmin = t1.MinPidLabel;
            }
            else
                Error("Invalid list operation", e);

            TypeLabel tl = new TypeLabel(t, pmax, pmin, sec);

            e.Label = tl;
            return tl;
        }

        public TypeLabel TypeCheck(Context c, List<Expression> es)
        {
            List<IPattern> p = new List<IPattern>();

            TypeLabel t = null;

            for (int i = 0; i < es.Count; i++)
            {
                if (es[i] is PatExpr)
                {
                    PatExpr pe = (PatExpr)es[i];
                    p.Add(pe.Pattern);
                    t = TypeCheck(c, pe.Expression);
                    c.AddMap(pe.Pattern, t);
                }
                else
                    t = TypeCheck(c, es[i]);
            }

            // remove all bound variables
            for (int i = p.Count - 1; i >= 0; i--)
                c.RemoveMap(p[i]);

            return t;
        }

        public TypeLabel TypeCheck(Context c, SeqExpr e)
        {
            TypeLabel tl = TypeCheck(c, e.Expressions);

            e.Label = tl;
            return tl;
        }

        public TypeLabel TypeCheck(Context c, ParenExpr e)
        {
            TypeLabel tl = TypeCheck(c, e.InnerExpression);

            e.Label = tl;
            return tl;
        }

        public TypeLabel TypeCheck(Context c, VarExpr e)
        {
            TypeLabel t = c.Get(e);

            if (t == null)
                Error("Unbound variable", e);

            TypeLabel tl = new TypeLabel(
                t.Type,
                (t.MaxPidLabel is PidRLabel) ? PidUtil.FromRestricted((PidRLabel)t.MaxPidLabel) : t.MaxPidLabel,
                (t.MinPidLabel is PidRLabel) ? PidUtil.FromRestricted((PidRLabel)t.MinPidLabel) : t.MaxPidLabel,
                (t.SecLabel is SecRLabel) ? SecUtil.FromRestricted((SecRLabel)t.SecLabel) : t.SecLabel
                );

            e.Label = tl;
            return tl;
        }

        public TypeLabel TypeCheck(Context c, SelfExpr e)
        {
            TypeLabel tl = new TypeLabel(
                new SimpleType(BaseType.Pid),
                new PidBase(null, new List<PidExpr>() { new PidExpr(c.Self, 0, 0) }),
                new PidBase(null, new List<PidExpr>() { new PidExpr(c.Self, 0, 0) }),
                new SecBase(null, null)
                );

            e.Label = tl;
            return tl;
        }

        public TypeLabel TypeCheck(Context c, ScOpExpr e)
        {
            TypeLabel t1 = TypeCheck(c, e.Left);
            SecLabel pc = c.PC;
            c.PC = SecUtil.Taint(c.PC, t1.SecLabel);
            TypeLabel t2 = TypeCheck(c, e.Right);
            c.PC = pc;

            // Check the types of both operands
            if (t1.Type != SimpleType.BoolType)
                Error("Expected a boolean, found " + t1.Type.ToString(), e);
            else if (t2.Type != SimpleType.BoolType)
                Error("Expected a boolean, found " + t2.Type.ToString(), e);

            // Check the operand
            if (e.Op != ScOp.OrElse || e.Op != ScOp.AndAlso)
                Error("Invalid short-circuit operation", e);

            TypeLabel tl = new TypeLabel(
                new SimpleType(BaseType.Bool),
                new PidBase(null, null),
                new PidBase(null, null),
                SecUtil.Taint(t2.SecLabel, t1.SecLabel)
                );

            e.Label = tl;
            return tl;
        }

        public TypeLabel TypeCheck(Context c, IfExpr e)
        {
            if (e.Clauses.Count == 0)
                Error("There must be at least one clause in an if statement", e);

            SecLabel initPc = c.PC;
            List<TypeLabel> labels = new List<TypeLabel>();
            List<TypeLabel> glabels = new List<TypeLabel>();

            for (int i = 0; i < e.Clauses.Count; i++)
            {
                TypeLabel grd = TypeCheckGuard(c, e.Clauses[i].Guard);
                c.PC = SecUtil.Taint(c.PC, grd.SecLabel);
                TypeLabel curr = TypeCheck(c, e.Clauses[i].Body);
                e.Clauses[i].Label = curr;
                labels.Add(curr);
                glabels.Add(grd);
            }

            Type t = labels[0].Type;
            for (int i = 1; i < labels.Count; i++)
            {
                if (labels[i].Type != t)
                    Error("Each branch should be of type " + t.ToString(), e);
            }

            // The last guard has the label T as it is "true" always, so ignore it
            SecLabel sec = labels.Last().SecLabel;
            // Now compute the label of the whole expression
            for (int i = labels.Count - 2; i >= 0; i--)
                sec = SecUtil.Taint(SecUtil.Meet(sec, labels[i].SecLabel), glabels[i].SecLabel);

            PidLabel pmax = labels[0].MaxPidLabel;
            PidLabel pmin = labels[0].MinPidLabel;

            for (int i = 1; i < labels.Count; i++)
            {
                pmax = PidUtil.Join(pmax, labels[i].MaxPidLabel);
                pmin = PidUtil.Meet(pmin, labels[i].MinPidLabel);
            }

            c.PC = initPc;

            TypeLabel tl = new TypeLabel(t, pmax, pmin, sec);

            e.Label = tl;
            return tl;
        }

        public TypeLabel TypeCheckGuard(Context c, List<List<Expression>> g)
        {
            if (g.Count == 0 || g[0].Count == 0)
                Error("A guard must have at least one expression", null);

            // All expressions should be boolean, and the return security label
            // should be the meet of all labels
            List<SecLabel> sec = new List<SecLabel>();

            for (int i = 0; i < g.Count; i++)
            {
                for (int j = 0; j < g[i].Count; j++)
                {
                    TypeLabel t = TypeCheck(c, g[i][j]);
                    if (t.Type != SimpleType.BoolType)
                        Error("Each expression in a guard must have a boolean type", g[i][j]);
                    sec.Add(t.SecLabel);
                }
            }

            // Now meet all the labels
            SecLabel s = sec[0];
            for (int i = 1; i < sec.Count; i++)
                s = SecUtil.Meet(s, sec[i]);

            return new TypeLabel(
                SimpleType.BoolType,
                new PidBase(null, null),
                new PidBase(null, null),
                s
                );
        }

        public TypeLabel TypeCheck(Context c, ListCaseExpr e)
        {
            SecLabel initPC = c.PC;

            // first type-check the list
            TypeLabel list = TypeCheck(c, e.List);
            if (!(list.Type is ListType))
                Error("First expression in a list case expression must be a list", e.List);

            // now taint the PC
            c.PC = SecUtil.Taint(c.PC, list.SecLabel);

            // type the nil case
            TypeLabel nil = TypeCheck(c, e.NilCase);

            // extend the context
            c.AddMap(e.HeadPattern, new TypeLabel(
                ((ListType)(list.Type)).ElementType,
                list.MaxPidLabel, list.MinPidLabel, list.SecLabel));
            c.AddMap(e.TailVar, list);

            // type the cons case
            TypeLabel cons = TypeCheck(c, e.ConsCase);

            c.RemoveMap(e.TailVar);
            c.RemoveMap(e.HeadPattern);
            c.PC = initPC;

            // check the branches have the same type
            if (nil.Type != cons.Type)
                Error("Branches of a list case statement must have the same type", e);

            TypeLabel tl = new TypeLabel(
                nil.Type,
                PidUtil.Join(nil.MaxPidLabel, cons.MaxPidLabel),
                PidUtil.Meet(nil.MinPidLabel, cons.MinPidLabel),
                SecUtil.Taint(SecUtil.Meet(nil.SecLabel, cons.SecLabel), list.SecLabel)
                );

            e.Label = tl;
            return tl;
        }

        public TypeLabel TypeCheck(Context c, RecordExpr e)
        {
            if (!c.Records.ContainsRecord(e.Name))
                Error("Undefined record " + e.Name, e);

            List<TypeLabel> labels = new List<TypeLabel>();
            labels.Add(new TypeLabel(
                new AtomType(e.Name),
                new PidBase(null, null),
                new PidBase(null, null),
                new SecBase(null, null)
                ));

            List<Tuple<string, Expression>> record = c.Records.Records[e.Name];
            for (int i = 0; i < record.Count; i++)
                labels.Add(TypeCheck(c, record[i].Item2));

            List<Type> t = new List<Type>();
            List<PidLabel> pmax = new List<PidLabel>();
            List<PidLabel> pmin = new List<PidLabel>();
            List<SecLabel> sec = new List<SecLabel>();

            for (int i = 0; i < labels.Count; i++)
            {
                t.Add(labels[i].Type);
                pmax.Add(labels[i].MaxPidLabel);
                pmin.Add(labels[i].MinPidLabel);
                sec.Add(labels[i].SecLabel);
            }

            TypeLabel tl = new TypeLabel(
                new TupleType(t),
                new PidTuple(pmax),
                new PidTuple(pmin),
                new SecTuple(sec)
                );

            e.Label = tl;
            return tl;
        }

        public TypeLabel TypeCheck(Context c, RecModExpr e)
        {
            if (!c.Records.ContainsRecord(e.Name))
                Error("Undefined record " + e.Name, e);

            // type-check the source record
            TypeLabel src = TypeCheck(c, e.Record);

            if (!((src.Type is TupleType) || (src.MaxPidLabel is PidLabel) ||
                (src.MinPidLabel is PidLabel) || (src.SecLabel is SecLabel)))
                Error("Invalid record expresion", e.Record);

            List<Type> tempt = ((TupleType)(src.Type)).Types;
            List<PidLabel> temppmax = ((PidTuple)(src.MaxPidLabel)).Labels;
            List<PidLabel> temppmin = ((PidTuple)(src.MinPidLabel)).Labels;
            List<SecLabel> tempsec = ((SecTuple)(src.SecLabel)).Labels;

            // now go through modifying each item
            for (int i = 0; i < e.Modifications.Count; i++)
            {
                int index = c.Records.IndexOfField(e.Name, e.Modifications[i].Name.Value);
                if (index < 0)
                    Error("Unknown record field " + e.Modifications[i].Name.Value, e);
                index++;

                if (index > tempt.Count - 1)
                    Error("Invalid record field", e);

                // check the types match
                TypeLabel newType = TypeCheck(c, e.Modifications[i].Contents);
                if (newType.Type != tempt[index])
                    Error("Type of new expression does not match record type", 
                        e.Modifications[i].Contents);

                // update the labels
                temppmax[index] = newType.MaxPidLabel;
                temppmin[index] = newType.MinPidLabel;
                tempsec[index] = newType.SecLabel;
            }

            TypeLabel tl = new TypeLabel(
                new TupleType(tempt),
                new PidTuple(temppmax),
                new PidTuple(temppmin),
                new SecTuple(tempsec)
                );

            e.Label = tl;
            return tl;
        }

        public TypeLabel TypeCheck(Context c, RecProjExpr e)
        {
            int index = c.Records.IndexOfField(e.Name, e.Field);
            if (index < 0)
                Error("Unknown record field", e);
            index++;

            TypeLabel t = TypeCheck(c, e.Record);

            if (!((t.Type is TupleType) || (t.MaxPidLabel is PidLabel) ||
                (t.MinPidLabel is PidLabel) || (t.SecLabel is SecLabel)))
                Error("Invalid record expresion", e.Record);

            if (index > ((TupleType)(t.Type)).Types.Count - 1)
                Error("Invalid record field", e);

            TypeLabel tl = new TypeLabel(
                ((TupleType)(t.Type)).Types[index],
                ((PidTuple)(t.MaxPidLabel)).Labels[index],
                ((PidTuple)(t.MinPidLabel)).Labels[index],
                ((SecTuple)(t.SecLabel)).Labels[index]
                );

            e.Label = tl;
            return tl;
        }

        public TypeLabel TypeCheck(Context c, FunctionExpr e)
        {
            Tuple<FunType, PidFun, PidFun, SecFun> args = this.functionStore.GetLabels(e.Name, e.ArgumentTypes);

            for (int i = 0; i < e.Arguments.Count; i++)
                c.AddMap(e.Arguments[i].Pattern, new TypeLabel(
                    args.Item1.Args[i], args.Item2.Args[i],
                    args.Item3.Args[i], args.Item4.Args[i]));

            TypeLabel ret = TypeCheck(c, e.Body);

            if (ret.Type != args.Item1.Ret)
                Error("Return type does not match specified type", e);

            for (int i = e.Arguments.Count - 1; i >= 0; i--)
                c.RemoveMap(e.Arguments[i].Pattern);

            TypeLabel tl = new TypeLabel(
                new FunType(args.Item1.Args, ret.Type),
                new PidFun(args.Item2.Args, ret.MaxPidLabel),
                new PidFun(args.Item3.Args, ret.MinPidLabel),
                new SecFun(args.Item4.Args, ret.SecLabel)
                );

            e.Label = tl;
            return tl;
        }

        public TypeLabel TypeCheck(Context c, FunExpr e)
        {
            List<PidRLabel> pmaxargs = this.funStore.GetFunPidMaxArg(e);
            List<PidRLabel> pminargs = this.funStore.GetFunPidMinArg(e);
            List<SecRLabel> secargs = this.funStore.GetFunSecArg(e);

            for (int i = 0; i < e.Arguments.Count; i++)
                c.AddMap(e.Arguments[i].Pattern, new TypeLabel(
                    e.Arguments[i].Type, pmaxargs[i], pminargs[i], secargs[i]));

            TypeLabel ret = TypeCheck(c, e.Body);

            for (int i = e.Arguments.Count - 1; i >= 0; i--)
                c.RemoveMap(e.Arguments[i].Pattern);

            TypeLabel tl = new TypeLabel(
                new FunType(e.ArgumentTypes, ret.Type),
                new PidFun(pmaxargs, ret.MaxPidLabel),
                new PidFun(pminargs, ret.MinPidLabel),
                new SecFun(secargs, ret.SecLabel)
                );

            e.Label = tl;
            return tl;
        }

        public TypeLabel TypeCheck(Context c, ApplyExpr e)
        {
            List<TypeLabel> argLabels = new List<TypeLabel>();

            for (int i = 0; i < e.Args.Count; i++)
                argLabels.Add(TypeCheck(c, e.Args[i]));

            List<Type> argTypes = new List<Type>();
            List<PidLabel> argPidMax = new List<PidLabel>();
            List<PidLabel> argPidMin = new List<PidLabel>();
            List<SecLabel> argSec = new List<SecLabel>();

            for (int i = 0; i < argLabels.Count; i++)
            {
                argTypes.Add(argLabels[i].Type);
                argPidMax.Add(argLabels[i].MaxPidLabel);
                argPidMin.Add(argLabels[i].MinPidLabel);
                argSec.Add(argLabels[i].SecLabel);
            }

            FunType f = null;
            PidFun pmax = null;
            PidFun pmin = null;
            SecFun sec = null;

            if (e.Function is AtomExpr)
            {
                string fName = ((AtomExpr)(e.Function)).Value;
                if (functionStore.ContainsFunction(fName, argTypes) < 0)
                    Error("A function with the name " + fName + " does not exist for the " +
                        "given argument types", e);

                Tuple<FunType, PidFun, PidFun, SecFun> tp = functionStore.GetLabels(fName, argTypes);
                f = tp.Item1;
                pmax = tp.Item2;
                pmin = tp.Item3;
                sec = tp.Item4;
            }
            else if (e.Function is FnRefExpr)
            {
                string fName = ((FnRefExpr)(e.Function)).Function;
                if (functionSpecs.ContainsFunction(fName, argTypes) < 0)
                    Error("A function spec with the name " + fName + " does not exist for the " +
                        "given argument types", e);

                Tuple<FunType, PidFun, PidFun, SecFun> tp = functionSpecs.GetLabels(fName, argTypes);
                f = tp.Item1;
                pmax = tp.Item2;
                pmin = tp.Item3;
                sec = tp.Item4;
            }
            else
            {
                TypeLabel fl = TypeCheck(c, e.Function);
                f = fl.Type as FunType;
                pmax = fl.MaxPidLabel as PidFun;
                pmin = fl.MinPidLabel as PidFun;
                sec = fl.SecLabel as SecFun;

                if (f == null || pmax == null || pmin == null || sec == null)
                    Error("Function does not have a valid function type", e.Function);

                // Check the type of the arguments
                if (f.Args.Count != argTypes.Count)
                    Error("Function has the wrong number of arguments", e.Function);
                for (int i = 0; i < f.Args.Count; i++)
                {
                    if (f.Args[i] != argTypes[i])
                        Error("Expected argument of type " + f.Args[i].ToString() +
                            ", found " + argTypes[i], e);
                }
            }

            // Now compute the process and security labels
            // First compute the substitution mapping the fn args onto the actual args
            Dictionary<PidVar, PidBase> pmaxSub = PidUtil.Unify(
                new PidRTuple(pmax.Args), new PidTuple(argPidMax));
            Dictionary<PidVar, PidBase> pminSub = PidUtil.Unify(
                new PidRTuple(pmin.Args), new PidTuple(argPidMin));
            Dictionary<SecVar, SecBase> secSub = SecUtil.Unify(
                new SecRTuple(sec.Args), new SecTuple(argSec));

            // return label is this substitution mapped onto the return type
            Type retType = f.Ret;
            PidLabel retPidMax = PidUtil.Sub(pmaxSub, pmax.Ret, true);
            PidLabel retPidMin = PidUtil.Sub(pminSub, pmin.Ret, false);
            SecLabel retSec = SecUtil.Sub(secSub, sec.Ret);

            TypeLabel tl = new TypeLabel(retType, retPidMax, retPidMin, retSec);
            e.Label = tl;
            return tl;
        }

        public TypeLabel TypeCheck(Context c, LabExpr e)
        {
            TypeLabel t = TypeCheck(c, e.Expr);
            List<TypeLabel> labs = new List<TypeLabel>();
            for (int i = 0; i < e.Labels.Count; i++)
            {
                TypeLabel tt = TypeCheck(c, e.Labels[i]);

                if (tt.Type != SimpleType.PidType)
                    Error("Labels must return a process identifier", e.Labels[i]);

                labs.Add(tt);
            }

            // Create the security label
            ISecPid owner = new PidExpr(c.Self, -1, -1);
            List<ISecPid> readers = new List<ISecPid>() { owner };

            for (int i = 0; i < labs.Count; i++)
            {
                PidBase p = labs[i].MinPidLabel as PidBase;

                if (p == null)
                    Error("Label is not valid for a process id expression", e.Labels[i]);

                if (p.Pidvs != null)
                {
                    foreach (PidVar v in p.Pidvs)
                        readers.Add(v);
                }

                if (p.Pids != null)
                {
                    foreach (PidExpr pe in p.Pids)
                        readers.Add(pe);
                }
            }

            TypeLabel tl = new TypeLabel(t.Type,
                new PidBase(null, null), new PidBase(null, null),
                new SecBase(null, new List<SecPolicy>() { new SecPolicy(owner, 
                    new List<ISecPid>(readers.Distinct())) }));
            e.Label = tl;
            return tl;
        }

        public TypeLabel TypeCheck(Context c, SpawnExpr e)
        {
            string oldSelf = c.Self;

            if (e.Pid == null)
                e.Pid = PidUtil.NewPid();

            c.Self = e.Pid.Pid;

            TypeCheck(c, new ApplyExpr(e.Function, e.Args, e.Function.Line, e.Function.Col));

            c.Self = oldSelf;

            TypeLabel tl = new TypeLabel(
                new SimpleType(BaseType.Pid),
                new PidBase(null, new List<PidExpr>() { e.Pid }),
                new PidBase(null, new List<PidExpr>() { e.Pid }),
                new SecBase(null, null)
                );
            e.Label = tl;
            return tl;
        }

        public TypeLabel TypeCheck(Context c, RxExpr e)
        {
            List<PidLabel> clausePMax = new List<PidLabel>();
            List<PidLabel> clausePMin = new List<PidLabel>();
            List<SecLabel> clauseSec = new List<SecLabel>();
            Type clauseRet = null;

            for (int i = 0; i < e.Clauses.Count; i++)
            {
                c.AddMap(e.Clauses[i].Pattern, new TypeLabel(
                    e.Clauses[i].Type, RxStore.GetRxPidMaxArg(e.Clauses[i]),
                    RxStore.GetRxPidMinArg(e.Clauses[i]), RxStore.GetRxSecArg(e.Clauses[i])));

                TypeLabel ct = TypeCheck(c, e.Clauses[i].Body);
                e.Clauses[i].Label = ct;

                if (clauseRet == null)
                    clauseRet = ct.Type;
                else if (clauseRet != ct.Type)
                    Error("Clause types do not match", e.Clauses[i]);

                clausePMax.Add(ct.MaxPidLabel);
                clausePMin.Add(ct.MinPidLabel);
                clauseSec.Add(ct.SecLabel);

                c.RemoveMap(e.Clauses[i].Pattern);
            }

            TypeLabel tl = new TypeLabel(
                clauseRet,
                PidUtil.Join(clausePMax),
                PidUtil.Meet(clausePMin),
                SecUtil.Meet(clauseSec)
                );

            e.Label = tl;
            return tl;
        }

        public TypeLabel TypeCheck(Context c, TxExpr e)
        {
            if (!TxExprs.Contains(e))
                TxExprs.Add(e);

            TypeLabel tx = TypeCheck(c, e.Pid);
            TypeLabel msg = TypeCheck(c, e.Val);

            if (tx.Type != SimpleType.PidType || !(tx.MaxPidLabel is PidBase))
                Error("Expression must return a process identifier", e.Pid);

            // Check that message is allowed to be transmitted
            Tuple<List<SecVar>, List<ISecPid>> readers = SecUtil.Taint(msg.SecLabel, c.PC).Readers();

            PidBase txp = (PidBase)tx.MaxPidLabel;

            // Check actual process id's
            if (readers.Item2 != null)
            {
                if (txp.Pids != null)
                {
                    foreach (PidExpr p in txp.Pids)
                    {
                        if (readers.Item2.IndexOf(p) < 0)
                            Error("Possible security breach, message is not permitted to be transmitted to process " + p, e);
                    }
                }
                if (txp.Pidvs != null)
                {
                    foreach (PidVar v in txp.Pidvs)
                    {
                        if (readers.Item2.IndexOf(v) < 0)
                            Error("Possible security breach, message is not permitted to be transmitted to process " + v, e);
                    }
                }
            }

            // check variables
            if (readers.Item1 != null && readers.Item1.Count > 0)
            {
                if (txp.Pids != null)
                    foreach (SecVar v in readers.Item1)
                        foreach (PidExpr p in txp.Pids)
                            this.AddConstraint(new SecConstraint(p, v));
                if (txp.Pidvs != null)
                    foreach (SecVar v in readers.Item1)
                        foreach (PidVar p in txp.Pidvs)
                            this.AddConstraint(new SecConstraint(p, v));
            }

            e.Label = msg;
            return msg;
        }
    }
}
